$\vdash$ $\forall$$A$, $B$:Type, $L$:(($A$$\rightarrow$($B$ + Top)) List). p{-}first($L$) $\in$ $A$$\rightarrow$($B$ + Top)